Nuprl Lemma : gcd_of_triple
2,24
postcript
pdf
a
,
b
,
c
,
x
,
y
:
.
GCD(
a
;
b
;
x
)
GCD(
x
;
c
;
y
)
y
|
a
&
y
|
b
&
y
|
c
& (
z
:
.
z
|
a
z
|
b
z
|
c
z
|
y
)
latex
Definitions
GCD(
a
;
b
;
y
)
,
P
Q
,
P
&
Q
,
Prop
,
b
|
a
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
divides
transitivity
,
divides
wf
origin
a, b, c, x, y:
.
GCD(x;c;y) y | a & y | b & y | c & (z:. z | a z | b z | c z | y) a, b, c, x, y:.
GCD(x;c;y) y | a & y | b & y | c & (z:. z | a z | b z | c z | y) Qx:A. B(x)
T